open Binding
open Syntax


type tree_expr =
	| Type of tree_type 
	| Term of tree_term 
 
 and tree_expr_pair = tree_expr * tree_expr
	
 and tree_type = 
	| T_TyArr of tree_expr_pair 
	| T_TyVar of type_var
	| T_TyAll of tree_expr_pair
  
  and type_var = 
	| T_FreeType of string
	| T_BoundedType of string
  
  and tree_term = inner_term * tree_type
  
  and inner_term = 
	| T_TmApp of tree_expr_pair
	| T_TmVar of term_var
	| T_TmAbs of tree_expr_pair
	| T_TmTAbs of tree_expr_pair
  
  and term_var =
	| T_FreeTerm of string
	| T_BoundedTerm of string		 
	| T_TmString of string
	| T_TmInt of int
	
	
	
val tree_of_type : context->ty->tree_type
val type_of_tree : tree_type->context->ty



val tree_of_term : context->term->tree_expr
val term_of_tree : tree_term->context->term

val tree_of_expr : context->t_Expr->tree_expr
val expr_of_tree : tree_expr->context->t_Expr


val free_term_vars : context->term->term list
val replace_all : tree_expr->tree_expr->tree_expr->tree_expr

val make_abstract_term : tree_term->tree_term->tree_term
val make_application_term : tree_term->tree_expr->tree_term
